(declare-fun _substvar_129_ () String)
(declare-fun _substvar_158_ () String)
(declare-const Str7 String)
(declare-const Str14 String)
(declare-const Str19 String)
(declare-const v12 Bool)
(declare-const v13 Bool)
(assert (or (str.suffixof (str.++ Str7 "xqxgqj" "" "vikfooqqlg") (str.++ (str.++ "" "" Str14 "yazjgr" "") _substvar_158_ "ysvbhg")) false (str.suffixof (str.++ "vvfmigelhu" Str19 "") Str14) false))
(check-sat)
